YES 23.219 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((minimum :: [Ratio Int ->  Ratio Int) :: [Ratio Int ->  Ratio Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((minimum :: [Ratio Int ->  Ratio Int) :: [Ratio Int ->  Ratio Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
min x y
 | x <= y
 = x
 | otherwise
 = y

is transformed to
min x y = min2 x y

min1 x y True = x
min1 x y False = min0 x y otherwise

min0 x y True = y

min2 x y = min1 x y (x <= y)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (minimum :: [Ratio Int ->  Ratio Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx4500), Succ(vx3101000)) → new_primPlusNat(vx4500, vx3101000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vx300000), vx310100) → new_primMulNat(vx300000, vx310100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not(Succ(vx30800), Succ(vx44900)) → new_not(vx30800, vx44900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(vx30, :(vx310, vx311)) → new_foldl(new_min1(vx30, vx310), vx311)

The TRS R consists of the following rules:

new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min113(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min147(vx31, Neg(Zero), Neg(Zero), vx34, Zero) → new_min152(vx31, Zero, Zero, vx34)
new_min191(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → new_min183(vx30100, :%(Neg(Succ(Zero)), Neg(Zero)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Zero), Pos(Zero)))
new_min1127(vx36, Neg(Zero), Neg(Succ(vx3800)), vx39, Zero) → :%(Neg(Succ(vx36)), Neg(Zero))
new_min157(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min141(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min162(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min144(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1115(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(Zero)), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min1104(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_not1(Zero) → new_not3
new_min160(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min127(vx30000, vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))))
new_min19(vx15, vx1600, vx1700, vx18, False) → new_min0(vx15, Succ(vx1600), Succ(vx1700), vx18)
new_min180(vx30100, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1125(vx30100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min167(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1142(vx30100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min168(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min1142(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min148(vx31, vx320, vx330, vx34) → :%(Neg(Succ(vx31)), Pos(vx320))
new_min146(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min147(vx31, Pos(vx320), Pos(vx330), vx34, Succ(vx2170)) → new_min148(vx31, vx320, vx330, vx34)
new_min1127(vx36, Neg(Succ(vx3700)), Pos(Succ(vx3800)), vx39, Zero) → new_min1149(vx36, vx3700, vx3800, vx39, new_not2(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_min147(vx31, Neg(Succ(vx3200)), Pos(Succ(vx3300)), vx34, Succ(vx2170)) → new_min134(vx31, vx3200, vx3300, vx34, new_not5(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200)), vx2170))
new_min1102(vx30100, False) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min147(vx31, Pos(Succ(vx3200)), Neg(Succ(vx3300)), vx34, Zero) → new_min135(vx31, vx3200, vx3300, vx34, new_not7(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min1110(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min147(vx31, Pos(Succ(vx3200)), Neg(Zero), vx34, Zero) → new_min139(vx31, vx3200, vx34)
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1149(vx36, vx3700, vx3800, vx39, False) → new_min03(vx36, Succ(vx3700), Succ(vx3800), vx39)
new_min16(vx15, Pos(Succ(vx1600)), Pos(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Pos(Succ(vx1600)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))
new_min169(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min110(vx15, vx1600, vx1700, vx18, True) → :%(Pos(Succ(vx15)), Pos(Succ(vx1600)))
new_min117(vx20, vx2200, vx23) → :%(Pos(Succ(vx20)), Neg(Zero))
new_min1123(vx30100, vx31000000, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1127(vx36, Pos(Zero), Pos(Zero), vx39, Succ(vx3080)) → :%(Pos(Zero), Neg(Succ(vx39)))
new_min11(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min154(vx31, vx3200, vx3300, vx34, True) → :%(Neg(Succ(vx31)), Neg(Succ(vx3200)))
new_min03(vx36, vx370, vx380, vx39) → :%(Pos(vx380), Neg(Succ(vx39)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min176(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min172(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min114(vx20, Neg(vx210), Neg(vx220), vx23, Succ(vx1300)) → new_min122(vx20, vx210, vx220, vx23)
new_min1136(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min1125(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min198(vx30100, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min132(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min156(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Neg(Succ(vx1600)), Neg(Succ(vx1700)), vx18, Zero) → new_min18(vx15, vx1600, vx1700, vx18, new_not1(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min143(vx36, vx3700, vx3800, vx39, True) → :%(Neg(Succ(vx36)), Pos(Succ(vx3700)))
new_min1110(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min158(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → new_min1143(vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min190(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min138(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → new_min1102(vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1143(vx30100, False) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min170(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1127(vx36, Pos(Zero), Neg(Succ(vx3800)), vx39, Zero) → :%(Neg(Succ(vx36)), Pos(Zero))
new_min147(vx31, Pos(Succ(vx3200)), Neg(Zero), vx34, Succ(vx2170)) → new_min139(vx31, vx3200, vx34)
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min199(vx30100, vx31000000, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min193(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min01(:%(Neg(Zero), Neg(Succ(vx30100))))
new_min114(vx20, Pos(Zero), Neg(Zero), vx23, Zero) → new_min121(vx20, vx23)
new_min1143(vx30100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min186(vx30100, False) → new_min01(:%(Pos(Zero), Pos(Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min1123(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Neg(vx160), Pos(vx170), vx18, Succ(vx460)) → new_min0(vx15, vx160, vx170, vx18)
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Succ(vx30000)), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Zero), Neg(Succ(vx30100))))
new_min143(vx36, vx3700, vx3800, vx39, False) → :%(Pos(Succ(vx3800)), Neg(Succ(vx39)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min1142(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_not1(Succ(vx4470)) → new_not5(Zero, vx4470)
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min114(vx20, Neg(Succ(vx2100)), Pos(Succ(vx2200)), vx23, Succ(vx1300)) → new_min116(vx20, vx2100, vx2200, vx23, new_not5(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100)), vx1300))
new_min158(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1127(vx36, Neg(Zero), Pos(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Neg(Zero))
new_min1140(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min147(vx31, Pos(Zero), Neg(Succ(vx3300)), vx34, Succ(vx2170)) → new_min136(vx31, vx3300, vx34)
new_min147(vx31, Neg(Zero), Pos(Zero), vx34, Zero) → new_min150(vx31, vx34)
new_min114(vx20, Pos(Succ(vx2100)), Neg(Zero), vx23, Succ(vx1300)) → new_min112(vx20, vx2100, vx23)
new_min1118(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min177(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_min1126(vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1122(vx30100, False) → new_min01(:%(Neg(Zero), Pos(Succ(vx30100))))
new_min190(vx30100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1120(vx30100, vx310100, False) → :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))
new_min144(vx30100, vx31000000, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min140(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1124(vx30100, vx31000000, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min114(vx20, Pos(Succ(vx2100)), Neg(Succ(vx2200)), vx23, Zero) → new_min119(vx20, vx2100, vx2200, vx23, new_not7(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_min199(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min123(vx20, vx2100, vx2200, vx23, False) → :%(Pos(Succ(vx2200)), Neg(Succ(vx23)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min146(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1128(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min16(vx15, Neg(Succ(vx1600)), Pos(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Neg(Succ(vx1600)))
new_min16(vx15, Neg(Succ(vx1600)), Neg(Succ(vx1700)), vx18, Succ(vx460)) → new_min18(vx15, vx1600, vx1700, vx18, new_not0(vx460, new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min133(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min130(vx30100, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min12(vx20, vx23) → :%(Pos(Succ(vx20)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min198(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min177(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min1106(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min196(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min1119(vx30100, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min114(vx20, Neg(Zero), Pos(Succ(vx2200)), vx23, Zero) → new_min117(vx20, vx2200, vx23)
new_min1114(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min1127(vx36, Pos(Succ(vx3700)), Neg(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Pos(Succ(vx3700)))
new_min1127(vx36, Neg(Succ(vx3700)), Neg(Succ(vx3800)), vx39, Succ(vx3080)) → new_min173(vx36, vx3700, vx3800, vx39, new_not0(vx3080, new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min16(vx15, Neg(Zero), Pos(Succ(vx1700)), vx18, Zero) → :%(Pos(Succ(vx15)), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min1145(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1126(vx30100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min192(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min184(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min132(vx30100, vx31000000, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_min183(vx30100, :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min1144(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1130(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min156(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min1131(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → new_min183(vx30100, :%(Pos(Zero), Pos(Succ(vx310100))))
new_min178(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Zero), Pos(Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Succ(vx30000)), Pos(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min190(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Neg(Zero), Neg(Succ(vx1700)), vx18, Zero) → :%(Pos(Succ(vx15)), Neg(Zero))
new_min116(vx20, vx2100, vx2200, vx23, False) → :%(Pos(Succ(vx2200)), Neg(Succ(vx23)))
new_min127(vx30000, vx30100, False) → new_min01(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))))
new_min1128(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1146(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min14(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min149(vx31, vx3300, vx34) → :%(Neg(Succ(vx31)), Neg(Zero))
new_primMulNat0(Succ(vx300000), vx310100) → new_primPlusNat1(new_primMulNat0(vx300000, vx310100), vx310100)
new_min163(vx30100, vx31000000, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min188(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min1147(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min147(vx31, Neg(vx320), Neg(vx330), vx34, Succ(vx2170)) → new_min152(vx31, vx320, vx330, vx34)
new_min1138(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min118(vx20, vx2100, vx23) → :%(Pos(Succ(vx20)), Neg(Succ(vx2100)))
new_min168(vx30100, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min0(vx15, vx160, vx170, vx18) → :%(Pos(vx170), Pos(Succ(vx18)))
new_min171(vx5, vx6, vx7, True) → :%(Pos(Zero), Pos(Succ(vx5)))
new_min15(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min147(vx31, Pos(Zero), Pos(Zero), vx34, Zero) → new_min148(vx31, Zero, Zero, vx34)
new_min00(vx15, vx160, vx170, vx18) → :%(Neg(vx170), Pos(Succ(vx18)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min168(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_min169(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min147(vx31, Neg(Zero), Pos(Zero), vx34, Succ(vx2170)) → new_min150(vx31, vx34)
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min1146(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1141(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min186(vx30100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → new_min1148(vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min16(vx15, Neg(Zero), Neg(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min1115(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))
new_min16(vx15, Neg(Zero), Neg(Zero), vx18, Succ(vx460)) → :%(Neg(Zero), Pos(Succ(vx18)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1127(vx36, Pos(Zero), Pos(Succ(vx3800)), vx39, Zero) → :%(Neg(Succ(vx36)), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))) → new_min1137(vx30100, vx310100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min1112(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min1127(vx36, Neg(Succ(vx3700)), Pos(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Neg(Succ(vx3700)))
new_min16(vx15, Pos(Succ(vx1600)), Neg(Succ(vx1700)), vx18, Zero) → new_min110(vx15, vx1600, vx1700, vx18, new_not2(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_min137(vx36, vx3700, vx3800, vx39, False) → new_min02(vx36, Succ(vx3700), Succ(vx3800), vx39)
new_min1127(vx36, Neg(Succ(vx3700)), Neg(Succ(vx3800)), vx39, Zero) → new_min173(vx36, vx3700, vx3800, vx39, new_not1(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_min1116(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min184(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min176(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min129(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min11(vx30100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min17(vx15, vx1600, vx1700, vx18, False) → :%(Pos(Succ(vx1700)), Pos(Succ(vx18)))
new_min147(vx31, Pos(Zero), Neg(Zero), vx34, Zero) → new_min151(vx31, vx34)
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min180(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min114(vx20, Neg(Zero), Pos(Succ(vx2200)), vx23, Succ(vx1300)) → new_min117(vx20, vx2200, vx23)
new_min144(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min16(vx15, Pos(Zero), Pos(Zero), vx18, Succ(vx460)) → :%(Pos(Zero), Pos(Succ(vx18)))
new_min172(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min125(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min151(vx31, vx34) → :%(Neg(Succ(vx31)), Pos(Zero))
new_min1127(vx36, Neg(vx370), Pos(vx380), vx39, Succ(vx3080)) → new_min03(vx36, vx370, vx380, vx39)
new_min1112(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min1117(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min189(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → new_min130(vx30100, vx310100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1141(vx30100, vx31000000, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min15(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min16(vx15, Pos(vx160), Neg(vx170), vx18, Succ(vx460)) → new_min00(vx15, vx160, vx170, vx18)
new_min17(vx15, vx1600, vx1700, vx18, True) → :%(Pos(Succ(vx15)), Pos(Succ(vx1600)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min175(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min196(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → new_min1134(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), vx301), :%(vx3100, Pos(Succ(vx310100)))) → new_min16(vx30000, vx301, vx3100, vx310100, new_primPlusNat1(new_primMulNat0(vx30000, vx310100), vx310100))
new_min1134(vx30000, vx30100, False) → :%(Neg(Succ(Zero)), Neg(Zero))
new_min120(vx20, vx2200, vx23) → :%(Pos(Succ(vx20)), Pos(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min128(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1131(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_primPlusNat1(Zero, vx310100) → Succ(vx310100)
new_min16(vx15, Pos(Succ(vx1600)), Pos(Zero), vx18, Succ(vx460)) → :%(Pos(Zero), Pos(Succ(vx18)))
new_min194(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min161(vx30100, vx310100, False) → :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min1100(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min1105(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min139(vx31, vx3200, vx34) → :%(Neg(Succ(vx31)), Pos(Succ(vx3200)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min1114(vx30100, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_not0(vx3080, Succ(vx4490)) → new_not8(vx3080, vx4490)
new_min16(vx15, Pos(Zero), Pos(Succ(vx1700)), vx18, Succ(vx460)) → :%(Pos(Succ(vx1700)), Pos(Succ(vx18)))
new_min165(vx30100, vx310100, False) → :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))
new_min142(vx31, vx3200, vx34) → :%(Neg(Succ(vx31)), Neg(Succ(vx3200)))
new_min124(vx20, vx2100, vx2200, vx23, False) → :%(Neg(Succ(vx2200)), Neg(Succ(vx23)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → new_min183(vx30100, :%(Neg(Succ(Zero)), Neg(Succ(vx310100))))
new_min173(vx36, vx3700, vx3800, vx39, True) → :%(Neg(Succ(vx36)), Neg(Succ(vx3700)))
new_min188(vx30100, vx31000000, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min147(vx31, Pos(Succ(vx3200)), Pos(Succ(vx3300)), vx34, Zero) → new_min153(vx31, vx3200, vx3300, vx34, new_not6(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_min147(vx31, Pos(Succ(vx3200)), Neg(Succ(vx3300)), vx34, Succ(vx2170)) → new_min135(vx31, vx3200, vx3300, vx34, new_not5(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200)), vx2170))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min1139(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1106(vx30100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min02(vx36, vx370, vx380, vx39) → :%(Neg(vx380), Neg(Succ(vx39)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min16(vx15, Neg(Zero), Neg(Succ(vx1700)), vx18, Succ(vx460)) → :%(Neg(Succ(vx1700)), Pos(Succ(vx18)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min141(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1107(vx30100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min16(vx15, Neg(Zero), Pos(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Neg(Zero))
new_min114(vx20, Neg(Succ(vx2100)), Neg(Succ(vx2200)), vx23, Zero) → new_min124(vx20, vx2100, vx2200, vx23, new_not6(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → new_min183(vx30100, :%(Neg(Succ(Zero)), Pos(Succ(vx310100))))
new_min147(vx31, Neg(Succ(vx3200)), Pos(Succ(vx3300)), vx34, Zero) → new_min134(vx31, vx3200, vx3300, vx34, new_not7(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_min147(vx31, Neg(Succ(vx3200)), Pos(Zero), vx34, Zero) → new_min142(vx31, vx3200, vx34)
new_min164(vx10) → vx10
new_min16(vx15, Pos(Succ(vx1600)), Pos(Succ(vx1700)), vx18, Zero) → new_min17(vx15, vx1600, vx1700, vx18, new_not1(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_min185(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min1127(vx36, Pos(Succ(vx3700)), Pos(Succ(vx3800)), vx39, Zero) → new_min143(vx36, vx3700, vx3800, vx39, new_not1(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))
new_min1105(vx30100, vx31000000, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_not0(vx3080, Zero) → new_not9
new_min154(vx31, vx3200, vx3300, vx34, False) → :%(Neg(Succ(vx3300)), Pos(Succ(vx34)))
new_min171(vx5, vx6, vx7, False) → :%(Pos(Succ(vx6)), Neg(Succ(vx7)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(Zero)), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min1122(vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1137(vx30100, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1127(vx36, Pos(Succ(vx3700)), Pos(Succ(vx3800)), vx39, Succ(vx3080)) → new_min143(vx36, vx3700, vx3800, vx39, new_not0(vx3080, new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))
new_min114(vx20, Neg(Zero), Neg(Zero), vx23, Zero) → new_min122(vx20, Zero, Zero, vx23)
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min145(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Pos(Zero), Neg(Succ(vx1700)), vx18, Zero) → :%(Pos(Succ(vx15)), Pos(Zero))
new_min1127(vx36, Pos(Zero), Pos(Succ(vx3800)), vx39, Succ(vx3080)) → :%(Pos(Succ(vx3800)), Neg(Succ(vx39)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min111(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1102(vx30100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(Zero)), Neg(Zero))
new_min123(vx20, vx2100, vx2200, vx23, True) → :%(Pos(Succ(vx20)), Pos(Succ(vx2100)))
new_min124(vx20, vx2100, vx2200, vx23, True) → :%(Pos(Succ(vx20)), Neg(Succ(vx2100)))
new_min161(vx30100, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min14(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_not2(Succ(vx4520)) → new_not9
new_min1120(vx30100, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_not6(Zero) → new_not3
new_min155(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min198(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min135(vx31, vx3200, vx3300, vx34, False) → :%(Neg(Succ(vx3300)), Pos(Succ(vx34)))
new_min1123(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min121(vx20, vx23) → :%(Pos(Succ(vx20)), Pos(Zero))
new_primPlusNat0(Succ(vx4500), Zero) → Succ(vx4500)
new_primPlusNat0(Zero, Succ(vx3101000)) → Succ(vx3101000)
new_min147(vx31, Neg(Zero), Pos(Succ(vx3300)), vx34, Zero) → new_min149(vx31, vx3300, vx34)
new_min1110(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → new_min183(vx30100, :%(Pos(Zero), Neg(Succ(vx310100))))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → new_min183(vx30100, :%(Neg(Zero), Pos(Succ(vx310100))))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min1135(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_not8(Succ(vx30800), Zero) → new_not9
new_min193(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min1127(vx36, Pos(Succ(vx3700)), Pos(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Pos(Succ(vx3700)))
new_min129(vx30100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min111(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min170(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1129(vx30000, vx30100, False) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min1109(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min10(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1114(vx30100, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_primMulNat0(Zero, vx310100) → Zero
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min155(vx30000, vx30100, False) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1117(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min159(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min1133(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1108(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1111(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min136(vx31, vx3300, vx34) → :%(Neg(Succ(vx31)), Pos(Zero))
new_min147(vx31, Pos(Zero), Neg(Succ(vx3300)), vx34, Zero) → new_min136(vx31, vx3300, vx34)
new_min181(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min111(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_not4True
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min01(:%(Pos(Zero), Neg(Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min1128(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min162(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min179(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min114(vx20, Pos(Succ(vx2100)), Pos(Zero), vx23, Zero) → new_min115(vx20, Succ(vx2100), Zero, vx23)
new_min114(vx20, Pos(Zero), Pos(Succ(vx2200)), vx23, Zero) → new_min115(vx20, Zero, Succ(vx2200), vx23)
new_min114(vx20, Neg(Zero), Pos(Zero), vx23, Succ(vx1300)) → new_min12(vx20, vx23)
new_min01(vx537) → :%(Pos(Succ(Zero)), Pos(Zero))
new_min114(vx20, Pos(Zero), Neg(Succ(vx2200)), vx23, Zero) → new_min120(vx20, vx2200, vx23)
new_min170(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min1103(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min116(vx20, vx2100, vx2200, vx23, True) → :%(Pos(Succ(vx20)), Neg(Succ(vx2100)))
new_min125(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min16(vx15, Pos(Succ(vx1600)), Pos(Succ(vx1700)), vx18, Succ(vx460)) → new_min17(vx15, vx1600, vx1700, vx18, new_not0(vx460, new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min114(vx20, Pos(vx210), Pos(vx220), vx23, Succ(vx1300)) → new_min115(vx20, vx210, vx220, vx23)
new_min141(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min1117(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_not8(Zero, Succ(vx44900)) → new_not10
new_min174(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1104(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min1109(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1121(vx30100, vx31000000, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1108(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min167(vx30100, vx31000000, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min199(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min1122(vx30100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min114(vx20, Pos(Succ(vx2100)), Pos(Succ(vx2200)), vx23, Zero) → new_min123(vx20, vx2100, vx2200, vx23, new_not6(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_min1135(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min192(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min18(vx15, vx1600, vx1700, vx18, False) → :%(Neg(Succ(vx1700)), Pos(Succ(vx18)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min176(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min1101(vx30100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1134(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1129(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1127(vx36, Neg(Zero), Neg(Zero), vx39, Succ(vx3080)) → :%(Neg(Zero), Neg(Succ(vx39)))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min177(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min195(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1148(vx30100, False) → :%(Neg(Succ(Zero)), Neg(Zero))
new_min1100(vx30100, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min16(vx15, Pos(Zero), Pos(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Pos(Zero))
new_not8(Succ(vx30800), Succ(vx44900)) → new_not8(vx30800, vx44900)
new_min1104(vx30100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1147(vx30100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1140(vx30100, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min140(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min145(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1113(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → new_min183(vx30100, :%(Neg(Zero), Neg(Succ(vx310100))))
new_min196(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1112(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min181(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1133(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min128(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), vx301), :%(vx3100, Pos(Succ(vx310100)))) → new_min147(vx30000, vx301, vx3100, vx310100, new_primPlusNat0(new_primMulNat0(vx30000, vx310100), Succ(vx310100)))
new_min130(vx30100, vx310100, False) → :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))
new_min126(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1130(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min1124(vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min1113(vx30100, vx31000000, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min131(vx30100, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_primPlusNat0(Zero, Zero) → Zero
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min1107(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_not5(Succ(vx4130), vx2170) → new_not8(vx4130, vx2170)
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min160(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1111(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min1121(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_not9False
new_min114(vx20, Neg(Zero), Pos(Zero), vx23, Zero) → new_min12(vx20, vx23)
new_min112(vx20, vx2100, vx23) → :%(Pos(Succ(vx20)), Pos(Succ(vx2100)))
new_min1107(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → new_min183(vx30100, :%(Pos(Zero), Pos(Zero)))
new_not6(Succ(vx3990)) → new_not10
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min138(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min195(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min119(vx20, vx2100, vx2200, vx23, True) → :%(Pos(Succ(vx20)), Pos(Succ(vx2100)))
new_min1119(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))
new_min13(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min189(vx30100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min110(vx15, vx1600, vx1700, vx18, False) → new_min00(vx15, Succ(vx1600), Succ(vx1700), vx18)
new_min193(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min175(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min133(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1127(vx36, Neg(Zero), Neg(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Neg(Zero))
new_not2(Zero) → new_not3
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min1141(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min147(vx31, Neg(Zero), Neg(Succ(vx3300)), vx34, Zero) → new_min152(vx31, Zero, Succ(vx3300), vx34)
new_min147(vx31, Neg(Succ(vx3200)), Neg(Zero), vx34, Zero) → new_min152(vx31, Succ(vx3200), Zero, vx34)
new_primPlusNat1(Succ(vx450), vx310100) → Succ(Succ(new_primPlusNat0(vx450, vx310100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min129(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1101(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min16(vx15, Neg(Succ(vx1600)), Pos(Succ(vx1700)), vx18, Zero) → new_min19(vx15, vx1600, vx1700, vx18, new_not2(new_primPlusNat0(new_primMulNat0(vx1700, vx1600), Succ(vx1600))))
new_not7(Zero) → new_not3
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min1130(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → new_min161(vx30100, vx310100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min137(vx36, vx3700, vx3800, vx39, True) → :%(Neg(Succ(vx36)), Pos(Succ(vx3700)))
new_min1127(vx36, Pos(Succ(vx3700)), Neg(Succ(vx3800)), vx39, Zero) → new_min137(vx36, vx3700, vx3800, vx39, new_not2(new_primPlusNat0(new_primMulNat0(vx3800, vx3700), Succ(vx3700))))
new_min1148(vx30100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min152(vx31, vx320, vx330, vx34) → :%(Neg(Succ(vx31)), Neg(vx320))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min197(vx30100, vx31000000, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1115(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_not3new_not4
new_min1146(vx30100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min166(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min114(vx20, Neg(Succ(vx2100)), Neg(Zero), vx23, Zero) → new_min122(vx20, Succ(vx2100), Zero, vx23)
new_min114(vx20, Neg(Zero), Neg(Succ(vx2200)), vx23, Zero) → new_min122(vx20, Zero, Succ(vx2200), vx23)
new_min1127(vx36, Neg(Zero), Pos(Succ(vx3800)), vx39, Zero) → :%(Neg(Succ(vx36)), Neg(Zero))
new_min1147(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min185(vx30100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1106(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min13(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), vx301), :%(vx3100, Neg(Succ(vx310100)))) → new_min1127(vx30000, vx301, vx3100, vx310100, new_primPlusNat0(new_primMulNat0(vx30000, vx310100), Succ(vx310100)))
new_min153(vx31, vx3200, vx3300, vx34, False) → :%(Pos(Succ(vx3300)), Pos(Succ(vx34)))
new_min1145(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1136(vx30100, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min135(vx31, vx3200, vx3300, vx34, True) → :%(Neg(Succ(vx31)), Pos(Succ(vx3200)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min181(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1125(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min01(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))))
new_min1113(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1131(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min172(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min16(vx15, Pos(Succ(vx1600)), Neg(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Pos(Succ(vx1600)))
new_min157(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min146(vx30100, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min191(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1103(vx30100, vx31000000, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1126(vx30100, False) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min11(vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min113(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min194(vx30000, vx30100, vx31000000, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min138(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → new_min1129(vx30000, vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))) → :%(Neg(Succ(Zero)), Neg(Succ(vx310100)))
new_min133(vx30100, vx31000000, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1133(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min1124(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min188(vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1144(vx30100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1139(vx30100, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1127(vx36, Pos(Succ(vx3700)), Pos(Zero), vx39, Succ(vx3080)) → :%(Pos(Zero), Neg(Succ(vx39)))
new_min197(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Neg(Zero))) → :%(Pos(Succ(Zero)), Neg(Zero))
new_min125(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min163(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_not8(Zero, Zero) → new_not3
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min1118(vx30100, vx31000000, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Succ(vx310100)))) → new_min165(vx30100, vx310100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min158(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min174(vx30000, vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min189(vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min165(vx30100, vx310100, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min1136(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1116(vx30100, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min114(vx20, Pos(Succ(vx2100)), Neg(Succ(vx2200)), vx23, Succ(vx1300)) → new_min119(vx20, vx2100, vx2200, vx23, new_not5(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100)), vx1300))
new_min153(vx31, vx3200, vx3300, vx34, True) → :%(Neg(Succ(vx31)), Pos(Succ(vx3200)))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min1116(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Zero))) → new_min1101(vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(vx310000)), Neg(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))) → new_min10(vx30100, vx31000000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Zero), Neg(Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Succ(vx30000)), Neg(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min167(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Succ(vx30000)), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Zero), Pos(Succ(vx30100))))
new_min162(vx30100, vx31000000, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1127(vx36, Neg(Zero), Neg(Succ(vx3800)), vx39, Succ(vx3080)) → :%(Neg(Succ(vx3800)), Neg(Succ(vx39)))
new_min1135(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min192(vx30000, vx30100, True) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min1100(vx30100, vx310100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min18(vx15, vx1600, vx1700, vx18, True) → :%(Pos(Succ(vx15)), Neg(Succ(vx1600)))
new_min1109(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min122(vx20, vx210, vx220, vx23) → :%(Pos(Succ(vx20)), Neg(vx210))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min1138(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))) → new_min182(vx30100, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min179(vx30100, vx31000000, vx310100, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min131(vx30100, vx310100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min180(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min1132(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min119(vx20, vx2100, vx2200, vx23, False) → :%(Neg(Succ(vx2200)), Neg(Succ(vx23)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min178(vx30000, vx30100, vx31000000, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min127(vx30000, vx30100, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min184(vx30100, vx310100, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min1132(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1127(vx36, Neg(Succ(vx3700)), Neg(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Neg(Succ(vx3700)))
new_min182(vx30100, vx310100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Succ(vx310100)))
new_min187(vx30100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min131(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min191(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_not7(Succ(vx4110)) → new_not0(vx4110, Zero)
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → new_min183(vx30100, :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → new_min183(vx30100, :%(Neg(Zero), Pos(Zero)))
new_min114(vx20, Pos(Succ(vx2100)), Neg(Zero), vx23, Zero) → new_min112(vx20, vx2100, vx23)
new_min10(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min140(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min1108(vx30000, vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Pos(Zero), Pos(Zero))
new_min1127(vx36, Pos(Zero), Neg(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Pos(Zero))
new_min183(vx12, vx13) → :%(Pos(Zero), Neg(Succ(vx12)))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min157(vx30000, vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min147(vx31, Neg(Succ(vx3200)), Neg(Succ(vx3300)), vx34, Zero) → new_min154(vx31, vx3200, vx3300, vx34, new_not6(new_primPlusNat0(new_primMulNat0(vx3300, vx3200), Succ(vx3200))))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min132(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min194(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))) → new_min1140(vx30100, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min126(vx30100, vx31000000, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Pos(Zero), Neg(Zero)))
new_min134(vx31, vx3200, vx3300, vx34, True) → :%(Neg(Succ(vx31)), Neg(Succ(vx3200)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Zero), Pos(Zero)))
new_min1105(vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min16(vx15, Neg(Succ(vx1600)), Neg(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Neg(Succ(vx1600)))
new_min187(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min182(vx30100, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min1121(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min114(vx20, Pos(Zero), Neg(Zero), vx23, Succ(vx1300)) → new_min121(vx20, vx23)
new_min1127(vx36, Pos(vx370), Neg(vx380), vx39, Succ(vx3080)) → new_min02(vx36, vx370, vx380, vx39)
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min166(vx30000, vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min1127(vx36, Neg(Succ(vx3700)), Neg(Zero), vx39, Succ(vx3080)) → :%(Neg(Zero), Neg(Succ(vx39)))
new_min1127(vx36, Pos(Zero), Pos(Zero), vx39, Zero) → :%(Neg(Succ(vx36)), Pos(Zero))
new_min150(vx31, vx34) → :%(Neg(Succ(vx31)), Neg(Zero))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Neg(Zero))) → new_min195(vx30000, vx30100, new_not7(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1145(vx30100, vx31000000, True) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min1111(vx30000, vx30100, vx31000000, new_not7(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min178(vx30000, vx30100, vx31000000, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_primPlusNat0(Succ(vx4500), Succ(vx3101000)) → Succ(Succ(new_primPlusNat0(vx4500, vx3101000)))
new_min147(vx31, Pos(Zero), Neg(Zero), vx34, Succ(vx2170)) → new_min151(vx31, vx34)
new_min114(vx20, Pos(Zero), Pos(Zero), vx23, Zero) → new_min115(vx20, Zero, Zero, vx23)
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min185(vx30100, new_not1(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Pos(Zero), Pos(Succ(vx1700)), vx18, Zero) → :%(Pos(Succ(vx15)), Pos(Zero))
new_min114(vx20, Neg(Succ(vx2100)), Pos(Zero), vx23, Succ(vx1300)) → new_min118(vx20, vx2100, vx23)
new_min1138(vx30100, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Zero))), Pos(Zero))) → new_min15(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), vx301), :%(vx3100, Neg(Succ(vx310100)))) → new_min114(vx30000, vx301, vx3100, vx310100, new_primPlusNat0(new_primMulNat0(vx30000, vx310100), Succ(vx310100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min114(vx20, Pos(Zero), Neg(Succ(vx2200)), vx23, Succ(vx1300)) → new_min120(vx20, vx2200, vx23)
new_min1119(vx30100, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min174(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Pos(Zero))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Succ(vx310100)))) → new_min179(vx30100, vx31000000, vx310100, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min134(vx31, vx3200, vx3300, vx34, False) → :%(Pos(Succ(vx3300)), Pos(Succ(vx34)))
new_min169(vx30000, vx30100, False) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1139(vx30100, vx310100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Succ(vx310100)))
new_min1149(vx36, vx3700, vx3800, vx39, True) → :%(Neg(Succ(vx36)), Neg(Succ(vx3700)))
new_min197(vx30100, vx31000000, vx310100, True) → :%(Pos(Zero), Neg(Succ(vx30100)))
new_min147(vx31, Neg(Zero), Pos(Succ(vx3300)), vx34, Succ(vx2170)) → new_min149(vx31, vx3300, vx34)
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Zero))) → new_min126(vx30100, vx31000000, new_not1(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Pos(Zero), Neg(Zero), vx18, Zero) → :%(Pos(Succ(vx15)), Pos(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Neg(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Neg(Zero))) → :%(Neg(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Succ(vx310100)))) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1103(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Succ(vx310100)))) → :%(Neg(Zero), Pos(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Zero))
new_min1(:%(Pos(Succ(vx30000)), Neg(Zero)), :%(Pos(Succ(vx310000)), Pos(Zero))) → :%(Pos(Succ(vx30000)), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Neg(Zero))) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero))) → new_min164(:%(Neg(Zero), Neg(Zero)))
new_min13(vx30100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_not10new_not4
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min01(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))))
new_min1(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → :%(Neg(Succ(Zero)), Pos(Zero))
new_min1144(vx30100, False) → :%(Pos(Succ(Succ(Zero))), Neg(Zero))
new_min1(:%(Neg(Succ(vx30000)), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Zero))) → new_min155(vx30000, vx30100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1137(vx30100, vx310100, False) → :%(Pos(Succ(Zero)), Neg(Succ(vx310100)))
new_min14(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1118(vx30100, vx31000000, vx310100, True) → :%(Neg(Zero), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Zero), Neg(Zero))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Zero), Pos(Zero))
new_min166(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min175(vx30000, vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Pos(Zero))
new_min128(vx30100, vx31000000, vx310100, False) → :%(Neg(Succ(Succ(Succ(vx31000000)))), Neg(Succ(vx310100)))
new_min114(vx20, Neg(Succ(vx2100)), Pos(Succ(vx2200)), vx23, Zero) → new_min116(vx20, vx2100, vx2200, vx23, new_not7(new_primPlusNat0(new_primMulNat0(vx2200, vx2100), Succ(vx2100))))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min171(vx30100, vx310000, vx310100, new_not6(new_primPlusNat0(new_primMulNat0(vx310000, vx30100), Succ(vx30100))))
new_min159(vx30100, vx31000000, False) → :%(Pos(Succ(Succ(Succ(vx31000000)))), Neg(Zero))
new_min19(vx15, vx1600, vx1700, vx18, True) → :%(Pos(Succ(vx15)), Neg(Succ(vx1600)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Neg(Succ(Zero)), Neg(Zero))) → :%(Neg(Succ(Zero)), Neg(Zero))
new_min114(vx20, Neg(Succ(vx2100)), Pos(Zero), vx23, Zero) → new_min118(vx20, vx2100, vx23)
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(:%(Pos(Succ(vx30000)), Neg(Succ(vx30100))), :%(Pos(Zero), Pos(Zero))) → :%(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(:%(Pos(Zero), Pos(Succ(vx30100))), :%(Pos(Succ(Zero)), Pos(Zero))) → new_min186(vx30100, new_not1(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Succ(Succ(vx31000000)))), Pos(Zero))) → new_min163(vx30100, vx31000000, new_not6(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(vx31000000, vx30100), Succ(vx30100)), Succ(vx30100)), Succ(vx30100))))
new_min16(vx15, Neg(Succ(vx1600)), Neg(Zero), vx18, Succ(vx460)) → :%(Neg(Zero), Pos(Succ(vx18)))
new_min1132(vx30000, vx30100, vx31000000, True) → :%(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min173(vx36, vx3700, vx3800, vx39, False) → :%(Neg(Succ(vx3800)), Neg(Succ(vx39)))
new_min147(vx31, Neg(Succ(vx3200)), Pos(Zero), vx34, Succ(vx2170)) → new_min142(vx31, vx3200, vx34)
new_min160(vx30000, vx30100, False) → new_min01(:%(Pos(Succ(vx30000)), Pos(Succ(vx30100))))
new_min1(:%(Neg(Zero), Neg(Succ(vx30100))), :%(Neg(Succ(Zero)), Pos(Succ(vx310100)))) → new_min1120(vx30100, vx310100, new_not6(new_primPlusNat0(Zero, Succ(vx30100))))
new_min1(:%(Neg(Succ(vx30000)), Pos(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min113(vx30000, vx30100, new_not6(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))
new_min145(vx30000, vx30100, False) → :%(Neg(Succ(Succ(Zero))), Neg(Zero))
new_min159(vx30100, vx31000000, True) → :%(Pos(Zero), Pos(Succ(vx30100)))
new_min115(vx20, vx210, vx220, vx23) → :%(Pos(Succ(vx20)), Pos(vx210))
new_min147(vx31, Pos(Zero), Pos(Succ(vx3300)), vx34, Zero) → new_min148(vx31, Zero, Succ(vx3300), vx34)
new_min147(vx31, Pos(Succ(vx3200)), Pos(Zero), vx34, Zero) → new_min148(vx31, Succ(vx3200), Zero, vx34)
new_not5(Zero, vx2170) → new_not10
new_min156(vx30000, vx30100, False) → :%(Pos(Succ(Succ(Zero))), Pos(Zero))
new_min1(:%(Pos(Zero), Neg(Succ(vx30100))), :%(Pos(Succ(Succ(Zero))), Pos(Zero))) → new_min187(vx30100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx30100)), Succ(vx30100))))

The set Q consists of the following terms:

new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_not7(Zero)
new_min160(x0, x1, True)
new_min163(x0, x1, False)
new_min137(x0, x1, x2, x3, False)
new_min1135(x0, x1, x2, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_min173(x0, x1, x2, x3, False)
new_min152(x0, x1, x2, x3)
new_min1132(x0, x1, x2, False)
new_min147(x0, Neg(x1), Neg(x2), x3, Succ(x4))
new_min1117(x0, x1, x2, True)
new_min114(x0, Pos(x1), Pos(x2), x3, Succ(x4))
new_min126(x0, x1, True)
new_min1127(x0, Pos(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_min147(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_min147(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_min1116(x0, x1, True)
new_min16(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_not8(Succ(x0), Succ(x1))
new_min174(x0, x1, True)
new_min1135(x0, x1, x2, False)
new_min1134(x0, x1, False)
new_min1110(x0, x1, True)
new_min165(x0, x1, False)
new_min1127(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_min03(x0, x1, x2, x3)
new_min110(x0, x1, x2, x3, True)
new_min13(x0, False)
new_min1129(x0, x1, False)
new_min1149(x0, x1, x2, x3, True)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min178(x0, x1, x2, True)
new_min114(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_min1127(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_min147(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_min139(x0, x1, x2)
new_min1127(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_min196(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_min176(x0, x1, False)
new_min138(x0, x1, False)
new_min131(x0, x1, False)
new_min114(x0, Neg(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_min178(x0, x1, x2, False)
new_min114(x0, Pos(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1101(x0, True)
new_min132(x0, x1, False)
new_min133(x0, x1, True)
new_min180(x0, x1, True)
new_min154(x0, x1, x2, x3, False)
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_min149(x0, x1, x2)
new_min11(x0, True)
new_min1126(x0, False)
new_min01(x0)
new_min1123(x0, x1, True)
new_min1138(x0, x1, True)
new_min124(x0, x1, x2, x3, False)
new_min1136(x0, x1, False)
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min1120(x0, x1, True)
new_min147(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_min129(x0, False)
new_min1119(x0, x1, True)
new_min1121(x0, x1, True)
new_min16(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_min114(x0, Neg(x1), Neg(x2), x3, Succ(x4))
new_min1111(x0, x1, x2, True)
new_min114(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_min114(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_min1108(x0, x1, x2, True)
new_min141(x0, x1, x2, True)
new_min188(x0, x1, False)
new_min129(x0, True)
new_min1127(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min1127(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min189(x0, True)
new_min1125(x0, False)
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min115(x0, x1, x2, x3)
new_min1112(x0, x1, True)
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min14(x0, x1, x2, False)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1127(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min1114(x0, x1, True)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_min16(x0, Neg(x1), Pos(x2), x3, Succ(x4))
new_min16(x0, Pos(x1), Neg(x2), x3, Succ(x4))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min16(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min16(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1124(x0, x1, False)
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min119(x0, x1, x2, x3, True)
new_min114(x0, Pos(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_min114(x0, Neg(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_min1110(x0, x1, False)
new_min114(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_min1(:%(Pos(Succ(x0)), x1), :%(x2, Neg(Succ(x3))))
new_min1(:%(Neg(Succ(x0)), x1), :%(x2, Pos(Succ(x3))))
new_min1148(x0, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min147(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1115(x0, x1, x2, False)
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min16(x0, Neg(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_min123(x0, x1, x2, x3, True)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_min1143(x0, False)
new_min120(x0, x1, x2)
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min1137(x0, x1, True)
new_min136(x0, x1, x2)
new_not7(Succ(x0))
new_min1122(x0, False)
new_min184(x0, x1, True)
new_min180(x0, x1, False)
new_min153(x0, x1, x2, x3, True)
new_min161(x0, x1, False)
new_min195(x0, x1, True)
new_primPlusNat0(Succ(x0), Zero)
new_min16(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min184(x0, x1, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_min18(x0, x1, x2, x3, True)
new_min1123(x0, x1, False)
new_min1117(x0, x1, x2, False)
new_min147(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_min147(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_min166(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_min147(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_min1(:%(Pos(Succ(x0)), x1), :%(x2, Pos(Succ(x3))))
new_min114(x0, Pos(Zero), Neg(Zero), x1, Succ(x2))
new_min114(x0, Neg(Zero), Pos(Zero), x1, Succ(x2))
new_min1138(x0, x1, False)
new_min113(x0, x1, False)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_min198(x0, x1, True)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1144(x0, False)
new_min1127(x0, Pos(x1), Neg(x2), x3, Succ(x4))
new_min1127(x0, Neg(x1), Pos(x2), x3, Succ(x4))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_primPlusNat0(Zero, Succ(x0))
new_min1139(x0, x1, False)
new_min163(x0, x1, True)
new_min155(x0, x1, True)
new_min183(x0, x1)
new_not6(Zero)
new_min1127(x0, Neg(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_min188(x0, x1, True)
new_min15(x0, x1, False)
new_min1108(x0, x1, x2, False)
new_min190(x0, False)
new_min16(x0, Pos(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_min193(x0, x1, True)
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1115(x0, x1, x2, True)
new_min179(x0, x1, x2, False)
new_min159(x0, x1, False)
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min1134(x0, x1, True)
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min194(x0, x1, x2, True)
new_min190(x0, True)
new_min17(x0, x1, x2, x3, False)
new_min10(x0, x1, x2, True)
new_min1102(x0, False)
new_min1144(x0, True)
new_min174(x0, x1, False)
new_min1127(x0, Pos(Zero), Pos(Zero), x1, Succ(x2))
new_min199(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_min191(x0, x1, x2, True)
new_min143(x0, x1, x2, x3, False)
new_min127(x0, x1, True)
new_min13(x0, True)
new_min1146(x0, False)
new_min1130(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min124(x0, x1, x2, x3, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Succ(x1))))
new_min156(x0, x1, False)
new_min175(x0, x1, x2, True)
new_min1127(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_min1127(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_min147(x0, Neg(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_min147(x0, Pos(Zero), Neg(Succ(x1)), x2, Succ(x3))
new_min185(x0, False)
new_primPlusNat0(Zero, Zero)
new_min1113(x0, x1, x2, True)
new_min14(x0, x1, x2, True)
new_min155(x0, x1, False)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_min1105(x0, x1, True)
new_min182(x0, x1, False)
new_min141(x0, x1, x2, False)
new_min138(x0, x1, True)
new_primMulNat0(Succ(x0), x1)
new_min165(x0, x1, True)
new_min160(x0, x1, False)
new_min123(x0, x1, x2, x3, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_min1129(x0, x1, True)
new_min114(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_min114(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_min1141(x0, x1, False)
new_min171(x0, x1, x2, True)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_min144(x0, x1, True)
new_min1119(x0, x1, False)
new_min172(x0, x1, x2, True)
new_min156(x0, x1, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Succ(x1))))
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min181(x0, x1, x2, False)
new_min116(x0, x1, x2, x3, False)
new_min147(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_min1109(x0, x1, x2, False)
new_min140(x0, x1, x2, False)
new_min158(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Zero), Neg(Zero)))
new_min1145(x0, x1, True)
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_min147(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_min16(x0, Pos(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_min147(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_not1(Succ(x0))
new_min191(x0, x1, x2, False)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(x1))))
new_not3
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min167(x0, x1, False)
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Succ(x1))))
new_min16(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min16(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_min1113(x0, x1, x2, False)
new_min145(x0, x1, True)
new_not2(Succ(x0))
new_min16(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_min135(x0, x1, x2, x3, False)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Zero), Pos(Zero)))
new_min150(x0, x1)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min192(x0, x1, True)
new_min134(x0, x1, x2, x3, False)
new_primMulNat0(Zero, x0)
new_min140(x0, x1, x2, True)
new_min0(x0, x1, x2, x3)
new_min1118(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Succ(x1))))
new_min169(x0, x1, True)
new_min137(x0, x1, x2, x3, True)
new_min128(x0, x1, x2, False)
new_min122(x0, x1, x2, x3)
new_min197(x0, x1, x2, False)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min157(x0, x1, False)
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min161(x0, x1, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_primPlusNat1(Succ(x0), x1)
new_min196(x0, x1, x2, True)
new_min1112(x0, x1, False)
new_min1127(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_not2(Zero)
new_min1131(x0, x1, True)
new_min17(x0, x1, x2, x3, True)
new_min114(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min1130(x0, x1, x2, True)
new_min114(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min1146(x0, True)
new_min114(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_min114(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_min1139(x0, x1, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min112(x0, x1, x2)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_min1149(x0, x1, x2, x3, False)
new_min114(x0, Neg(Succ(x1)), Pos(Zero), x2, Zero)
new_min114(x0, Pos(Succ(x1)), Neg(Zero), x2, Zero)
new_min1142(x0, True)
new_not8(Zero, Zero)
new_min1100(x0, x1, False)
new_not6(Succ(x0))
new_min16(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min1127(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_min1127(x0, Neg(Zero), Neg(Zero), x1, Succ(x2))
new_min1104(x0, False)
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1136(x0, x1, True)
new_min12(x0, x1)
new_min1106(x0, True)
new_primPlusNat0(Succ(x0), Succ(x1))
new_min1116(x0, x1, False)
new_min187(x0, True)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min185(x0, True)
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Zero)))
new_min1133(x0, x1, False)
new_min199(x0, x1, x2, True)
new_min1127(x0, Pos(Zero), Pos(Succ(x1)), x2, Succ(x3))
new_min114(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min195(x0, x1, False)
new_min127(x0, x1, False)
new_min00(x0, x1, x2, x3)
new_min1128(x0, x1, True)
new_min02(x0, x1, x2, x3)
new_min1131(x0, x1, False)
new_min162(x0, x1, False)
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Succ(x0))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Succ(x0))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Succ(x0))))
new_min177(x0, x1, x2, True)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_min131(x0, x1, True)
new_min1121(x0, x1, False)
new_min16(x0, Neg(Zero), Neg(Succ(x1)), x2, Zero)
new_min1114(x0, x1, False)
new_min114(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_min166(x0, x1, x2, True)
new_min159(x0, x1, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_not5(Zero, x0)
new_min1137(x0, x1, False)
new_min10(x0, x1, x2, False)
new_min144(x0, x1, False)
new_min179(x0, x1, x2, True)
new_min172(x0, x1, x2, False)
new_min154(x0, x1, x2, x3, True)
new_min147(x0, Neg(Succ(x1)), Pos(Zero), x2, Succ(x3))
new_min147(x0, Pos(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_min1127(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_min1147(x0, True)
new_min145(x0, x1, False)
new_min133(x0, x1, False)
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Succ(x1)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Succ(x1)), Neg(Zero)))
new_min1109(x0, x1, x2, True)
new_min153(x0, x1, x2, x3, False)
new_min1103(x0, x1, True)
new_min132(x0, x1, True)
new_min169(x0, x1, False)
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min147(x0, Pos(x1), Pos(x2), x3, Succ(x4))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min177(x0, x1, x2, False)
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Zero))), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min16(x0, Neg(Zero), Neg(Zero), x1, Succ(x2))
new_primPlusNat1(Zero, x0)
new_min1105(x0, x1, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_not5(Succ(x0), x1)
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_min168(x0, x1, True)
new_min125(x0, x1, x2, False)
new_min176(x0, x1, True)
new_min1124(x0, x1, True)
new_min197(x0, x1, x2, True)
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min142(x0, x1, x2)
new_min1107(x0, False)
new_min111(x0, x1, x2, False)
new_min1140(x0, x1, True)
new_min16(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_not8(Succ(x0), Zero)
new_min186(x0, True)
new_min164(x0)
new_min170(x0, x1, x2, False)
new_not0(x0, Succ(x1))
new_min117(x0, x1, x2)
new_min111(x0, x1, x2, True)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Zero), Neg(Zero)))
new_min157(x0, x1, True)
new_min147(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_min147(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_min1111(x0, x1, x2, False)
new_min16(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_min16(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_min11(x0, False)
new_min192(x0, x1, False)
new_min175(x0, x1, x2, False)
new_min1118(x0, x1, x2, True)
new_min1(:%(Neg(Succ(x0)), x1), :%(x2, Neg(Succ(x3))))
new_min16(x0, Pos(Zero), Pos(Zero), x1, Succ(x2))
new_not1(Zero)
new_min1141(x0, x1, True)
new_min116(x0, x1, x2, x3, True)
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_min126(x0, x1, False)
new_min113(x0, x1, True)
new_min16(x0, Neg(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_min147(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min1100(x0, x1, True)
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Pos(Succ(x1)), Neg(Succ(x2))))
new_min16(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_min1127(x0, Pos(Zero), Neg(Zero), x1, Zero)
new_min1127(x0, Neg(Zero), Pos(Zero), x1, Zero)
new_not4
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(:%(Neg(Zero), Neg(Zero)), :%(Neg(Succ(x0)), Pos(Succ(x1))))
new_min15(x0, x1, True)
new_min130(x0, x1, False)
new_min171(x0, x1, x2, False)
new_min114(x0, Pos(Succ(x1)), Pos(Zero), x2, Zero)
new_min1140(x0, x1, False)
new_not0(x0, Zero)
new_not8(Zero, Succ(x0))
new_min1127(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_min110(x0, x1, x2, x3, False)
new_min16(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_min193(x0, x1, False)
new_min1101(x0, False)
new_min1125(x0, True)
new_min1126(x0, True)
new_min1103(x0, x1, False)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min1142(x0, False)
new_min148(x0, x1, x2, x3)
new_min167(x0, x1, True)
new_min158(x0, x1, x2, True)
new_min1(:%(Neg(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Pos(Zero)))
new_min134(x0, x1, x2, x3, True)
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min1132(x0, x1, x2, True)
new_min114(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_min147(x0, Pos(Zero), Pos(Succ(x1)), x2, Zero)
new_min194(x0, x1, x2, False)
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Zero)), Neg(Zero)))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min186(x0, False)
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Zero)), Neg(Zero)))
new_min125(x0, x1, x2, True)
new_min1127(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Succ(x4))
new_min16(x0, Neg(Succ(x1)), Neg(Zero), x2, Zero)
new_min1120(x0, x1, False)
new_min147(x0, Pos(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min147(x0, Neg(Succ(x1)), Pos(Succ(x2)), x3, Zero)
new_min1122(x0, True)
new_min114(x0, Neg(Succ(x1)), Neg(Succ(x2)), x3, Zero)
new_min1127(x0, Pos(Succ(x1)), Pos(Succ(x2)), x3, Succ(x4))
new_min147(x0, Neg(Zero), Neg(Zero), x1, Zero)
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Zero))), Pos(Zero)))
new_min1148(x0, True)
new_min1107(x0, True)
new_min114(x0, Pos(Zero), Pos(Zero), x1, Zero)
new_min182(x0, x1, True)
new_min18(x0, x1, x2, x3, False)
new_min168(x0, x1, False)
new_min19(x0, x1, x2, x3, False)
new_min146(x0, x1, True)
new_min1128(x0, x1, False)
new_min118(x0, x1, x2)
new_min162(x0, x1, True)
new_min1(:%(Neg(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Neg(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Succ(x1))), :%(Pos(Succ(Succ(Succ(x2)))), Pos(Zero)))
new_min1106(x0, False)
new_min1102(x0, True)
new_min1127(x0, Neg(Succ(x1)), Neg(Zero), x2, Succ(x3))
new_min1147(x0, False)
new_min1127(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_min1127(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Zero), Pos(Succ(x0))))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Pos(Succ(x1)), Pos(Zero)))
new_min1104(x0, True)
new_not10
new_min1145(x0, x1, False)
new_min1143(x0, True)
new_min19(x0, x1, x2, x3, True)
new_not9
new_min181(x0, x1, x2, True)
new_min1133(x0, x1, True)
new_min143(x0, x1, x2, x3, True)
new_min173(x0, x1, x2, x3, True)
new_min151(x0, x1)
new_min1(:%(Neg(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Neg(Zero)))
new_min146(x0, x1, False)
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min1(:%(Pos(Succ(x0)), Neg(Zero)), :%(Pos(Zero), Neg(Zero)))
new_min1(:%(Neg(Succ(x0)), Pos(Zero)), :%(Neg(Zero), Pos(Zero)))
new_min198(x0, x1, False)
new_min147(x0, Pos(Zero), Neg(Zero), x1, Succ(x2))
new_min147(x0, Neg(Zero), Pos(Zero), x1, Succ(x2))
new_min189(x0, False)
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Neg(Zero)))
new_min1(:%(Pos(Zero), Pos(Zero)), :%(Neg(Succ(x0)), Pos(Zero)))
new_min1(:%(Neg(Zero), Pos(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_min1(:%(Pos(Zero), Neg(Zero)), :%(Pos(Succ(x0)), Pos(Zero)))
new_min128(x0, x1, x2, True)
new_min121(x0, x1)
new_min130(x0, x1, True)
new_min135(x0, x1, x2, x3, True)
new_min170(x0, x1, x2, True)
new_min187(x0, False)
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min1(:%(Pos(Zero), Neg(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1(:%(Neg(Zero), Neg(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Pos(Succ(x2))))
new_min1(:%(Pos(Zero), Pos(Succ(x0))), :%(Neg(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min1(:%(Neg(Zero), Pos(Succ(x0))), :%(Pos(Succ(Succ(Succ(x1)))), Neg(Succ(x2))))
new_min16(x0, Neg(Zero), Pos(Succ(x1)), x2, Zero)
new_min16(x0, Pos(Zero), Neg(Succ(x1)), x2, Zero)
new_min119(x0, x1, x2, x3, False)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: